package fos

import scala.util.parsing.input.Positional

/** Abstract Syntax Trees for terms. */
abstract class Term extends Positional

case object True extends Term {
  override val toString = "true"
}

case object False extends Term {
  override val toString = "false"
}
case object Zero extends Term {
  override val toString = "0"
}

case class IsZero(t: Term) extends Term {
    override val toString = "iszero " + t
}

case class If(t1: Term, t2: Term, t3: Term) extends Term {
  override val toString = "if %s then %s else %s".format(t1,t2,t3)
}

case class Succ(t: Term) extends Term {
    override val toString: String = try getValue.toString catch { case _ => "succ " + t }
    private def getValue: Int = if (t==Zero) 1 else if (t.isInstanceOf[Succ]) (t.asInstanceOf[Succ].getValue + 1) else throw new Exception
}

case class Pred(t: Term) extends Term {
    override val toString = "pred " + t
}

case class Variable(val name: String) extends Term {
  override def toString = name
}

case class Abstraction(x: Variable, ty: Type, t: Term) extends Term {
  override val toString = "(\\%s:%s. %s)".format(x,ty,t)
}

case class Application(t1: Term, t2: Term) extends Term {
  override val toString = t2 match {
    case _: Application => "%s (%s)".format(t1,t2)
    case _ => "%s %s".format(t1,t2)
  }
}

case class Let(let_v: Variable, let_ty: Type, let_t1: Term, let_t2: Term) extends Application(Abstraction(let_v,let_ty,let_t2),let_t1)

case class LetRec(rec_v: Variable, rec_ty: Type, rec_t1: Term, rec_t2: Term) extends Let(rec_v,rec_ty,Fix(Abstraction(rec_v,rec_ty,rec_t2)),rec_t2)

case class Pair(t1: Term, t2: Term) extends Term {
  override val toString = "{%s,%s}".format(t1,t2)
}

case class First(t: Term) extends Term {
  override val toString = "fst %s".format(t)
}

case class Second(t: Term) extends Term {
  override val toString = "snd %s".format(t)
}

case class InjectLeft(t: Term, ty: Type) extends Term {
    override val toString = "inl %s as %s".format(t,ty)
}

case class InjectRight(t: Term, ty: Type) extends Term {
    override val toString = "inl %s as %s".format(t,ty)
}

case class Case(t: Term, xl: Variable, tl: Term, xr: Variable, tr: Term) extends Term {
    override val toString = "case %s of inl %s=>%s| inr %s=>%s".format(t,xl,tl,xr,tr)
}

case class Fix(t: Term) extends Term {
    override val toString = "fix %s".format(t)
}

/** Abstract Syntax Trees for types. */
abstract class Type extends Term

case object TypeBool extends Type {
  override def toString() = "Bool"
}

case object TypeNumeric extends Type {
  override def toString() = "Nat"
}

object TypeFunction {   
  override def toString() = "Function"
}
case class TypeFunction(t1: Type, t2: Type) extends Type {
  override val toString = t1 match{
    case _: TypeFunction => "(%s)->%s".format(t1,t2)
    case _ => "%s->%s".format(t1,t2)
  }
}

object TypePair {   
  override def toString() = "Pair"
}
case class TypePair(t1: Type, t2: Type) extends Type {
  override val toString = t1 match{
    case _: TypePair => "(%s)*%s".format(t1,t2)
    case _: TypeSum => "(%s)*%s".format(t1,t2)
    case _ => "%s*%s".format(t1,t2)
  }
}

object TypeSum {   
  override def toString() = "Sum"
}
case class TypeSum(t1: Type, t2: Type) extends Type {
  override val toString = t1 match{
    case _: TypeSum => "(%s)+%s".format(t1,t2)
    case _: TypePair => "(%s)+%s".format(t1,t2)
    case _ => "%s+%s".format(t1,t2)
  }
}
